Nuprl Lemma : divisor_bound
2,24
postcript
pdf
a
:
,
b
:
.
a
|
b
a
b
latex
Definitions
P
Q
,
b
|
a
,
x
:
A
.
B
(
x
)
,
,
t
T
,
,
x
:
A
.
B
(
x
)
,
A
B
,
i
j
,
P
Q
,
A
,
False
Lemmas
mul
preserves
le
,
nat
wf
,
nat
plus
wf
,
divides
wf
origin
a:
, b:
. a | b 
a
b a:, b:. a | b ab Qx:A. B(x)
T
x:A. B(x)B
j
Q
A